Nuprl Lemma : symmetric_rel_or
4,23
postcript
pdf
T
:Type,
R1
,
R2
:(
T
T
Prop).
(Sym
x
,
y
:
T
.
x
R1
y
)
(Sym
x
,
y
:
T
.
x
R2
y
)
(Sym
x
,
y
:
T
.
x
(
R1
R2
)
y
)
latex
Definitions
R1
R2
,
Sym
x
,
y
:
T
.
E
(
x
;
y
)
,
Prop
,
P
Q
,
{
T
}
,
t
T
,
x
f
y
,
x
:
A
.
B
(
x
)
,
P
Q
origin
T:Type, R1, R2:(T
TProp).
(Sym x,y:T. x R2 y) (Sym x,y:T. x (R1 
R2) y) T:Type, R1, R2:(TTProp).
(Sym x,y:T. x R2 y) (Sym x,y:T. x (R1 R2) y) R2 Q
Tx:A. B(x) Q